(set-logic QF_AUFBV)
(set-info :source |These benchmarks are derived from a semi-automated proof of functional equivalence between two implementations of an Elliptic Curve Digital Signature Algorithm (ECDSA). More information about problem they encode can be found here: http://cps-vo.org/node/3405|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x196 () (_ BitVec 1))
(declare-fun x194 () (_ BitVec 1))
(declare-fun x192 () (_ BitVec 1))
(declare-fun x190 () (_ BitVec 1))
(declare-fun x188 () (_ BitVec 1))
(declare-fun x186 () (_ BitVec 1))
(declare-fun x184 () (_ BitVec 1))
(declare-fun x182 () (_ BitVec 1))
(declare-fun x181 () (_ BitVec 1))
(declare-fun x180 () (_ BitVec 384))
(declare-fun x179 () (_ BitVec 384))
(declare-fun x178 () (_ BitVec 1))
(declare-fun x176 () (_ BitVec 1))
(declare-fun x175 () (_ BitVec 1))
(declare-fun x174 () (_ BitVec 384))
(declare-fun x173 () (_ BitVec 384))
(declare-fun x171 () (_ BitVec 1))
(declare-fun x169 () (_ BitVec 1))
(declare-fun x167 () (_ BitVec 1))
(declare-fun x166 () (_ BitVec 1))
(declare-fun x165 () (_ BitVec 384))
(declare-fun x164 () (_ BitVec 384))
(declare-fun x163 () (_ BitVec 384))
(declare-fun x162 () (_ BitVec 384))
(declare-fun x160 () (_ BitVec 1))
(declare-fun x158 () (_ BitVec 1))
(declare-fun x156 () (_ BitVec 1))
(declare-fun x154 () (_ BitVec 1))
(declare-fun x152 () (_ BitVec 1))
(declare-fun x150 () (_ BitVec 1))
(declare-fun x149 () (_ BitVec 1))
(declare-fun x148 () (_ BitVec 384))
(declare-fun x147 () (_ BitVec 384))
(declare-fun x145 () (_ BitVec 1))
(declare-fun x143 () (_ BitVec 1))
(declare-fun x141 () (_ BitVec 1))
(declare-fun x140 () (_ BitVec 1))
(declare-fun x139 () (_ BitVec 384))
(declare-fun x138 () (_ BitVec 384))
(declare-fun x136 () (_ BitVec 1))
(declare-fun x134 () (_ BitVec 1))
(declare-fun x133 () (_ BitVec 1))
(declare-fun x131 () (_ BitVec 1))
(declare-fun x130 () (_ BitVec 1))
(declare-fun x128 () (_ BitVec 1))
(declare-fun x126 () (_ BitVec 1))
(declare-fun x124 () (_ BitVec 1))
(declare-fun x122 () (_ BitVec 1))
(declare-fun x121 () (_ BitVec 1))
(declare-fun x120 () (_ BitVec 384))
(declare-fun x119 () (_ BitVec 384))
(declare-fun x118 () (_ BitVec 1))
(declare-fun x116 () (_ BitVec 1))
(declare-fun x114 () (_ BitVec 1))
(declare-fun x113 () (_ BitVec 1))
(declare-fun x111 () (_ BitVec 1))
(declare-fun x109 () (_ BitVec 1))
(declare-fun x108 () (_ BitVec 1))
(declare-fun x107 () (_ BitVec 384))
(declare-fun x106 () (_ BitVec 384))
(declare-fun x105 () (_ BitVec 384))
(declare-fun x104 () (_ BitVec 384))
(declare-fun x103 () (_ BitVec 384))
(declare-fun x102 () (_ BitVec 384))
(declare-fun x101 () (_ BitVec 384))
(declare-fun x100 () (_ BitVec 1))
(declare-fun x99 () (_ BitVec 384))
(declare-fun x97 () (_ BitVec 1))
(declare-fun x96 () (_ BitVec 1))
(declare-fun x95 () (_ BitVec 64))
(declare-fun x94 () (_ BitVec 64))
(declare-fun x93 () (_ BitVec 64))
(declare-fun x92 () (_ BitVec 1))
(declare-fun x91 () (_ BitVec 64))
(declare-fun x90 () (_ BitVec 1))
(declare-fun x88 () (_ BitVec 1))
(declare-fun x86 () (_ BitVec 1))
(declare-fun x84 () (_ BitVec 1))
(declare-fun x82 () (_ BitVec 1))
(declare-fun x80 () (_ BitVec 1))
(declare-fun x79 () (_ BitVec 1))
(declare-fun x77 () (_ BitVec 1))
(declare-fun x75 () (_ BitVec 1))
(declare-fun x73 () (_ BitVec 1))
(declare-fun x72 () (_ BitVec 1))
(declare-fun x71 () (_ BitVec 1))
(declare-fun x70 () (_ BitVec 64))
(declare-fun x69 () (_ BitVec 64))
(declare-fun x68 () (_ BitVec 32))
(declare-fun x67 () (_ BitVec 32))
(declare-fun x66 () (_ BitVec 1))
(declare-fun x65 () (_ BitVec 384))
(declare-fun x64 () (_ BitVec 448))
(declare-fun x63 () (_ BitVec 384))
(declare-fun x62 () (_ BitVec 64))
(declare-fun x61 () (_ BitVec 1))
(declare-fun x60 () (_ BitVec 64))
(declare-fun x59 () (_ BitVec 64))
(declare-fun x58 () (_ BitVec 448))
(declare-fun x57 () (_ BitVec 64))
(declare-fun x56 () (_ BitVec 448))
(declare-fun x55 () (_ BitVec 32))
(declare-fun x54 () (_ BitVec 384))
(declare-fun x53 () (_ BitVec 448))
(declare-fun x52 () (_ BitVec 64))
(declare-fun x51 () (_ BitVec 448))
(declare-fun x50 () (_ BitVec 32))
(declare-fun x49 () (_ BitVec 384))
(declare-fun x48 () (_ BitVec 448))
(declare-fun x47 () (_ BitVec 64))
(declare-fun x46 () (_ BitVec 448))
(declare-fun x45 () (_ BitVec 32))
(declare-fun x44 () (_ BitVec 384))
(declare-fun x43 () (_ BitVec 448))
(declare-fun x42 () (_ BitVec 64))
(declare-fun x41 () (_ BitVec 448))
(declare-fun x40 () (_ BitVec 32))
(declare-fun x39 () (_ BitVec 384))
(declare-fun x38 () (_ BitVec 448))
(declare-fun x37 () (_ BitVec 64))
(declare-fun x36 () (_ BitVec 448))
(declare-fun x35 () (_ BitVec 32))
(declare-fun x34 () (_ BitVec 384))
(declare-fun x33 () (_ BitVec 448))
(declare-fun x32 () (_ BitVec 64))
(declare-fun x31 () (_ BitVec 448))
(declare-fun x30 () (_ BitVec 32))
(declare-fun x29 () (_ BitVec 384))
(declare-fun x28 () (_ BitVec 448))
(declare-fun x27 () (_ BitVec 64))
(declare-fun x26 () (_ BitVec 448))
(declare-fun x25 () (_ BitVec 32))
(declare-fun x24 () (_ BitVec 384))
(declare-fun x23 () (_ BitVec 448))
(declare-fun x22 () (_ BitVec 64))
(declare-fun x21 () (_ BitVec 448))
(declare-fun x20 () (_ BitVec 32))
(declare-fun x19 () (_ BitVec 384))
(declare-fun x18 () (_ BitVec 448))
(declare-fun x17 () (_ BitVec 64))
(declare-fun x16 () (_ BitVec 448))
(declare-fun x15 () (_ BitVec 384))
(declare-fun x14 () (_ BitVec 448))
(declare-fun x13 () (_ BitVec 64))
(declare-fun x12 () (_ BitVec 448))
(declare-fun x11 () (_ BitVec 384))
(declare-fun x10 () (_ BitVec 448))
(declare-fun x9 () (_ BitVec 64))
(declare-fun x8 () (_ BitVec 448))
(declare-fun x7 () (_ BitVec 32))
(declare-fun x6 () (_ BitVec 384))
(declare-fun x5 () (_ BitVec 448))
(declare-fun x4 ((_ BitVec 384) (_ BitVec 32) (_ BitVec 32) (_ BitVec 64) (_ BitVec 64)) (_ BitVec 448))
(declare-fun x3 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 384))
(declare-fun x1 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun x0 () (_ BitVec 64))
(declare-fun p197 () Bool)
(declare-fun p195 () Bool)
(declare-fun p193 () Bool)
(declare-fun p191 () Bool)
(declare-fun p189 () Bool)
(declare-fun p187 () Bool)
(declare-fun p185 () Bool)
(declare-fun p183 () Bool)
(declare-fun p177 () Bool)
(declare-fun p172 () Bool)
(declare-fun p170 () Bool)
(declare-fun p168 () Bool)
(declare-fun p161 () Bool)
(declare-fun p159 () Bool)
(declare-fun p157 () Bool)
(declare-fun p155 () Bool)
(declare-fun p153 () Bool)
(declare-fun p151 () Bool)
(declare-fun p146 () Bool)
(declare-fun p144 () Bool)
(declare-fun p142 () Bool)
(declare-fun p137 () Bool)
(declare-fun p135 () Bool)
(declare-fun p132 () Bool)
(declare-fun p129 () Bool)
(declare-fun p127 () Bool)
(declare-fun p125 () Bool)
(declare-fun p123 () Bool)
(declare-fun p117 () Bool)
(declare-fun p115 () Bool)
(declare-fun p112 () Bool)
(declare-fun p110 () Bool)
(declare-fun p98 () Bool)
(declare-fun p89 () Bool)
(declare-fun p87 () Bool)
(declare-fun p85 () Bool)
(declare-fun p83 () Bool)
(declare-fun p81 () Bool)
(declare-fun p78 () Bool)
(declare-fun p76 () Bool)
(declare-fun p74 () Bool)
(assert (= p197 (and p129 p195)))
(assert (= x196 (bvand x128 x194)))
(assert (= p195 (or (= x60 (_ bv0 64)) p193)))
(assert (= x194 (bvor x130 x192)))
(assert (= p193 (and p157 p191)))
(assert (= x192 (bvand x156 x190)))
(assert (= p191 (or p159 p189)))
(assert (= x190 (bvor x158 x188)))
(assert (= p189 (and p168 p187)))
(assert (= x188 (bvand x167 x186)))
(assert (= p187 (or p170 p185)))
(assert (= x186 (bvor x169 x184)))
(assert (= p185 (and p177 p183)))
(assert (= x184 (bvand x176 x182)))
(assert (= p183 (or (= x60 (_ bv0 64)) (= x179 x180))))
(assert (= x182 (bvor x178 x181)))
(assert (= x181 (ite (= x179 x180) (_ bv1 1) (_ bv0 1))))
(assert (= x180 (bvsub x102 x103)))
(assert (= x179 (bvsub x162 x163)))
(assert (= x178 (ite (= x60 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= p177 (or p172 (= x173 x174))))
(assert (= x176 (bvor x171 x175)))
(assert (= x175 (ite (= x173 x174) (_ bv1 1) (_ bv0 1))))
(assert (= x174 ((_ extract 447 64) x64)))
(assert (= x173 (bvsub x162 x163)))
(assert (= p172 (not (= x60 (_ bv0 64)))))
(assert (= x171 (bvnot x72)))
(assert (= p170 (and p112 p115)))
(assert (= x169 (bvand x111 x114)))
(assert (= p168 (or p161 (= x164 x165))))
(assert (= x167 (bvor x160 x166)))
(assert (= x166 (ite (= x164 x165) (_ bv1 1) (_ bv0 1))))
(assert (= x165 (bvsub x105 x106)))
(assert (= x164 (bvsub x162 x163)))
(assert (= x163 (bvneg (_ bv1388124618062372383947042015309946732620727252194336364173 384))))
(assert (= x162 (bvsub x102 x103)))
(assert (= p161 (or (= x60 (_ bv0 64)) (= x95 (_ bv0 64)))))
(assert (= x160 (bvor x90 x96)))
(assert (= p159 (and (= x70 (_ bv0 64)) p74)))
(assert (= x158 (bvand x71 x73)))
(assert (= p157 (or p135 p155)))
(assert (= x156 (bvor x134 x154)))
(assert (= p155 (and p142 p153)))
(assert (= x154 (bvand x141 x152)))
(assert (= p153 (or p144 p151)))
(assert (= x152 (bvor x143 x150)))
(assert (= p151 (or p146 (= x147 x148))))
(assert (= x150 (bvor x145 x149)))
(assert (= x149 (ite (= x147 x148) (_ bv1 1) (_ bv0 1))))
(assert (= x148 ((_ extract 447 64) x64)))
(assert (= x147 (bvsub x102 x103)))
(assert (= p146 (not (= x60 (_ bv0 64)))))
(assert (= x145 (bvnot x72)))
(assert (= p144 (and p112 p115)))
(assert (= x143 (bvand x111 x114)))
(assert (= p142 (or p137 (= x138 x139))))
(assert (= x141 (bvor x136 x140)))
(assert (= x140 (ite (= x138 x139) (_ bv1 1) (_ bv0 1))))
(assert (= x139 (bvsub x105 x106)))
(assert (= x138 (bvsub x102 x103)))
(assert (= p137 (or (= x60 (_ bv0 64)) (= x95 (_ bv0 64)))))
(assert (= x136 (bvor x90 x96)))
(assert (= p135 (or p132 (= x60 (_ bv0 64)))))
(assert (= x134 (bvor x131 x133)))
(assert (= x133 (ite (= x60 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= p132 (not (= x70 (_ bv0 64)))))
(assert (= x131 (bvnot x79)))
(assert (= x130 (ite (= x60 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= p129 (or p89 p127)))
(assert (= x128 (bvor x88 x126)))
(assert (= p127 (and p110 p125)))
(assert (= x126 (bvand x109 x124)))
(assert (= p125 (or p117 p123)))
(assert (= x124 (bvor x116 x122)))
(assert (= p123 (or (= x60 (_ bv0 64)) (= x119 x120))))
(assert (= x122 (bvor x118 x121)))
(assert (= x121 (ite (= x119 x120) (_ bv1 1) (_ bv0 1))))
(assert (= x120 (bvsub x102 x103)))
(assert (= x119 ((_ extract 447 64) x64)))
(assert (= x118 (ite (= x60 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= p117 (and p112 p115)))
(assert (= x116 (bvand x111 x114)))
(assert (= p115 (not (= x95 (_ bv0 64)))))
(assert (= x114 (bvnot x113)))
(assert (= x113 (ite (= x95 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= p112 (not (= x60 (_ bv0 64)))))
(assert (= x111 (bvnot x72)))
(assert (= p110 (or p98 (= x99 x107))))
(assert (= x109 (bvor x97 x108)))
(assert (= x108 (ite (= x99 x107) (_ bv1 1) (_ bv0 1))))
(assert (= x107 (bvsub x105 x106)))
(assert (= x106 (bvneg (_ bv1388124618062372383947042015309946732620727252194336364173 384))))
(assert (= x105 (ite (= x60 (_ bv0 64)) x101 x104)))
(assert (= x104 (bvsub x102 x103)))
(assert (= x103 (bvneg (_ bv1388124618062372383947042015309946732620727252194336364173 384))))
(assert (= x102 ((_ extract 447 64) x64)))
(assert (= x101 ((_ extract 447 64) x64)))
(assert (= x100 (ite (= x60 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= x99 ((_ extract 447 64) x64)))
(assert (= p98 (or (= x60 (_ bv0 64)) (= x95 (_ bv0 64)))))
(assert (= x97 (bvor x90 x96)))
(assert (= x96 (ite (= x95 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= x95 (bvadd x91 x94)))
(assert (= x94 (ite (bvule x63 x65) (_ bv0 64) x93)))
(assert (= x93 (bvneg (_ bv1 64))))
(assert (= x92 (ite (bvule x63 x65) (_ bv1 1) (_ bv0 1))))
(assert (= x91 (bvadd x0 x59)))
(assert (= x90 (ite (= x60 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= p89 (not (= x60 (_ bv0 64)))))
(assert (= x88 (bvnot x72)))
(assert (= p87 (or p78 p85)))
(assert (= x86 (bvor x77 x84)))
(assert (= p85 (and p81 p83)))
(assert (= x84 (bvand x80 x82)))
(assert (= p83 (not (= x60 (_ bv0 64)))))
(assert (= x82 (bvnot x72)))
(assert (= p81 (not (= x70 (_ bv0 64)))))
(assert (= x80 (bvnot x79)))
(assert (= x79 (ite (= x70 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= p78 (or (= x60 (_ bv0 64)) p76)))
(assert (= x77 (bvor x61 x75)))
(assert (= p76 (and (= x70 (_ bv0 64)) p74)))
(assert (= x75 (bvand x71 x73)))
(assert (= p74 (not (= x60 (_ bv0 64)))))
(assert (= x73 (bvnot x72)))
(assert (= x72 (ite (= x60 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= x71 (ite (= x70 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= x70 (bvadd x62 x69)))
(assert (= x69 ((_ sign_extend 32) x68)))
(assert (= x68 (ite (bvule x63 x65) (_ bv0 32) x67)))
(assert (= x67 (bvneg (_ bv1 32))))
(assert (= x66 (ite (bvule x63 x65) (_ bv1 1) (_ bv0 1))))
(assert (= x65 ((_ extract 447 64) x64)))
(assert (= x64 (x4 x54 x55 (_ bv11 32) x0 x57)))
(assert (= x63 (bvneg (_ bv1388124618062372383947042015309946732620727252194336364173 384))))
(assert (= x62 (bvadd x0 x59)))
(assert (= x61 (ite (= x60 (_ bv0 64)) (_ bv1 1) (_ bv0 1))))
(assert (= x60 (bvadd x0 x59)))
(assert (= x59 ((_ extract 63 0) x58)))
(assert (= x58 (x4 x54 x55 (_ bv11 32) x0 x57)))
(assert (= x57 ((_ extract 63 0) x56)))
(assert (= x56 (x4 x49 x50 (_ bv10 32) x0 x52)))
(assert (= x55 (bvneg (_ bv1 32))))
(assert (= x54 ((_ extract 447 64) x53)))
(assert (= x53 (x4 x49 x50 (_ bv10 32) x0 x52)))
(assert (= x52 ((_ extract 63 0) x51)))
(assert (= x51 (x4 x44 x45 (_ bv9 32) x0 x47)))
(assert (= x50 (bvneg (_ bv1 32))))
(assert (= x49 ((_ extract 447 64) x48)))
(assert (= x48 (x4 x44 x45 (_ bv9 32) x0 x47)))
(assert (= x47 ((_ extract 63 0) x46)))
(assert (= x46 (x4 x39 x40 (_ bv8 32) x0 x42)))
(assert (= x45 (bvneg (_ bv1 32))))
(assert (= x44 ((_ extract 447 64) x43)))
(assert (= x43 (x4 x39 x40 (_ bv8 32) x0 x42)))
(assert (= x42 ((_ extract 63 0) x41)))
(assert (= x41 (x4 x34 x35 (_ bv7 32) x0 x37)))
(assert (= x40 (bvneg (_ bv1 32))))
(assert (= x39 ((_ extract 447 64) x38)))
(assert (= x38 (x4 x34 x35 (_ bv7 32) x0 x37)))
(assert (= x37 ((_ extract 63 0) x36)))
(assert (= x36 (x4 x29 x30 (_ bv6 32) x0 x32)))
(assert (= x35 (bvneg (_ bv1 32))))
(assert (= x34 ((_ extract 447 64) x33)))
(assert (= x33 (x4 x29 x30 (_ bv6 32) x0 x32)))
(assert (= x32 ((_ extract 63 0) x31)))
(assert (= x31 (x4 x24 x25 (_ bv5 32) x0 x27)))
(assert (= x30 (bvneg (_ bv1 32))))
(assert (= x29 ((_ extract 447 64) x28)))
(assert (= x28 (x4 x24 x25 (_ bv5 32) x0 x27)))
(assert (= x27 ((_ extract 63 0) x26)))
(assert (= x26 (x4 x19 x20 (_ bv4 32) x0 x22)))
(assert (= x25 (bvneg (_ bv949793407 32))))
(assert (= x24 ((_ extract 447 64) x23)))
(assert (= x23 (x4 x19 x20 (_ bv4 32) x0 x22)))
(assert (= x22 ((_ extract 63 0) x21)))
(assert (= x21 (x4 x15 (_ bv1478102450 32) (_ bv3 32) x0 x17)))
(assert (= x20 (bvneg (_ bv197710369 32))))
(assert (= x19 ((_ extract 447 64) x18)))
(assert (= x18 (x4 x15 (_ bv1478102450 32) (_ bv3 32) x0 x17)))
(assert (= x17 ((_ extract 63 0) x16)))
(assert (= x16 (x4 x11 (_ bv1219536762 32) (_ bv2 32) x0 x13)))
(assert (= x15 ((_ extract 447 64) x14)))
(assert (= x14 (x4 x11 (_ bv1219536762 32) (_ bv2 32) x0 x13)))
(assert (= x13 ((_ extract 63 0) x12)))
(assert (= x12 (x4 x6 x7 (_ bv1 32) x0 x9)))
(assert (= x11 ((_ extract 447 64) x10)))
(assert (= x10 (x4 x6 x7 (_ bv1 32) x0 x9)))
(assert (= x9 ((_ extract 63 0) x8)))
(assert (= x8 (x4 x2 x3 (_ bv0 32) x0 (_ bv0 64))))
(assert (= x7 (bvneg (_ bv320071318 32))))
(assert (= x6 ((_ extract 447 64) x5)))
(assert (= x5 (x4 x2 x3 (_ bv0 32) x0 (_ bv0 64))))
(assert (= x3 (bvneg (_ bv859494029 32))))
(assert (= x2 (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (concat (select x1 (_ bv11 4)) (select x1 (_ bv10 4))) (select x1 (_ bv9 4))) (select x1 (_ bv8 4))) (select x1 (_ bv7 4))) (select x1 (_ bv6 4))) (select x1 (_ bv5 4))) (select x1 (_ bv4 4))) (select x1 (_ bv3 4))) (select x1 (_ bv2 4))) (select x1 (_ bv1 4))) (select x1 (_ bv0 4)))))
(assert true)
(assert (= (select x1 (_ bv15 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv14 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv13 4)) (_ bv0 32)))
(assert (= (select x1 (_ bv12 4)) (_ bv0 32)))
(assert (not (=> p87 p197)))
(check-sat)
(exit)
